Nuprl Lemma : vlnk_wf
11,40
postcript
pdf
i
,
j
,
x
:Id. link_
x
from
i
to
j
IdLnk
latex
Definitions
Id
,
t
T
,
<
a
,
b
>
,
x
:
A
.
B
(
x
)
,
link_
x
from
i
to
j
,
IdLnk
Lemmas
Id
wf
origin
i, j, x:Id. link_x from i to j 
IdLnk i, j, x:Id. link_x from i to j IdLnk Tx:A. B(x)